es:ES, e:E. state after e = (discrete state after e)  discrete state@loc(e) 

latex

Definitions	Atom$n, Type, Void, t  T, x:A.B(x), Top, x:A. B(x), b, A, b, , s = t, , loc(e), vartype(i;x), (x after e), discrete(i;x), x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, Id, x.A(x), (discrete state after e), state after e, discrete state@i, ES, E, <a, b>
Lemmas	es-E wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-isconst wf, es-after wf, subtype rel self, es-vartype wf, es-loc wf, bool wf, bnot wf, not wf, assert wf, equal-top